Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[move-prover] Fix a bug in treatment of type reflection in spec funs #15606

Merged
merged 1 commit into from
Dec 16, 2024
Merged

[move-prover] Fix a bug in treatment of type reflection in spec funs #15606

merged 1 commit into from
Dec 16, 2024

Conversation

wrwg
Copy link
Contributor

@wrwg wrwg commented Dec 15, 2024

Description

When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now.

Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.

How Has This Been Tested?

New test variant

@trunk-io Trunk.io
Copy link

trunk-io bot commented Dec 15, 2024 •
edited
Loading

⏱️ 1h 33m total CI duration on this PR
Slowest 15 Jobs Cumulative Duration Recent Runs
execution-performance / single-node-performance 22m 🟩 
rust-move-tests 13m 🟩 
rust-move-tests 13m 🟩 
rust-move-tests 13m 🟩 
rust-doc-tests 6m 🟩 
rust-cargo-deny 5m 🟩 🟩 🟩 
execution-performance / test-target-determinator 4m 🟩 
test-target-determinator 4m 🟩 
check 4m 🟩 
check-dynamic-deps 3m 🟩 🟩 🟩 
fetch-last-released-docker-image-tag 2m 🟩 
general-lints 1m 🟩 🟩 🟩 
semgrep/ci 1m 🟩 🟩 🟩 
file_change_determinator 32s 🟩 🟩 🟩 
permission-check 18s 🟩 🟩 🟩 

settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io

@wrwg Graphite App
Copy link
Contributor Author

wrwg commented Dec 15, 2024

This stack of pull requests is managed by Graphite. Learn more about stacking.

@wrwg
[move-prover] Fix a bug in treatment of type reflection in spec funs
19a9a10 
When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now.

Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
@wrwg wrwg requested review from rahxephon89 and vineethk December 15, 2024 17:20
@wrwg wrwg marked this pull request as ready for review December 15, 2024 17:20
@wrwg wrwg enabled auto-merge (squash) December 16, 2024 03:12
@github-actions GitHub Actions

This comment has been minimized.

Sign in to view
@github-actions GitHub Actions

This comment has been minimized.

Sign in to view
@github-actions GitHub Actions

This comment has been minimized.

Sign in to view
@github-actions GitHub Actions
Copy link
Contributor

✅ Forge suite compat success on 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5

Compatibility test results for 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5 (PR)
1. Check liveness of validators at old version: 3c6e693a27339e73520f41030dce8fc9cd504967
compatibility::simple-validator-upgrade::liveness-check : committed: 8710.02 txn/s, submitted: 8710.32 txn/s, expired: 0.31 txn/s, latency: 2049.51 ms, (p50: 2100 ms, p70: 2100, p90: 2500 ms, p99: 3300 ms), latency samples: 534801
2. Upgrading first Validator to new version: 19a9a1088d794667502fc76319f04648bd9f6ac5
compatibility::simple-validator-upgrade::single-validator-upgrading : committed: 6121.55 txn/s, latency: 4560.71 ms, (p50: 4600 ms, p70: 5600, p90: 6800 ms, p99: 6900 ms), latency samples: 112160
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 7161.44 txn/s, latency: 4598.32 ms, (p50: 4900 ms, p70: 5000, p90: 5200 ms, p99: 5600 ms), latency samples: 238300
3. Upgrading rest of first batch to new version: 19a9a1088d794667502fc76319f04648bd9f6ac5
compatibility::simple-validator-upgrade::half-validator-upgrading : committed: 5532.08 txn/s, latency: 5327.17 ms, (p50: 4600 ms, p70: 6900, p90: 7500 ms, p99: 7600 ms), latency samples: 104560
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 7083.65 txn/s, latency: 4636.50 ms, (p50: 4900 ms, p70: 5000, p90: 5300 ms, p99: 5600 ms), latency samples: 237620
4. upgrading second batch to new version: 19a9a1088d794667502fc76319f04648bd9f6ac5
compatibility::simple-validator-upgrade::rest-validator-upgrading : committed: 12279.52 txn/s, latency: 2211.28 ms, (p50: 2300 ms, p70: 2500, p90: 2900 ms, p99: 3000 ms), latency samples: 215220
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 12277.29 txn/s, latency: 2486.30 ms, (p50: 2400 ms, p70: 2800, p90: 3000 ms, p99: 3200 ms), latency samples: 406360
5. check swarm health
Compatibility test for 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5 passed
Test Ok

@github-actions GitHub Actions
Copy link
Contributor

✅ Forge suite realistic_env_max_load success on 19a9a1088d794667502fc76319f04648bd9f6ac5

two traffics test: inner traffic : committed: 14567.49 txn/s, latency: 2728.70 ms, (p50: 2700 ms, p70: 2700, p90: 3000 ms, p99: 3300 ms), latency samples: 5538880
two traffics test : committed: 99.89 txn/s, latency: 1382.42 ms, (p50: 1300 ms, p70: 1400, p90: 1500 ms, p99: 1600 ms), latency samples: 1720
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 1.627, avg: 1.567", "ConsensusProposalToOrdered: max: 0.334, avg: 0.297", "ConsensusOrderedToCommit: max: 0.305, avg: 0.296", "ConsensusProposalToCommit: max: 0.598, avg: 0.592"]
Max non-epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.66s no progress at version 31502 (avg 0.20s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.57s no progress at version 2849081 (avg 0.57s) [limit 16].
Test Ok

@github-actions GitHub Actions
Copy link
Contributor

✅ Forge suite framework_upgrade success on 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5

Compatibility test results for 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5 (PR)
Upgrade the nodes to version: 19a9a1088d794667502fc76319f04648bd9f6ac5
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1416.39 txn/s, submitted: 1417.52 txn/s, failed submission: 1.13 txn/s, expired: 1.13 txn/s, latency: 2130.25 ms, (p50: 2100 ms, p70: 2100, p90: 2700 ms, p99: 4100 ms), latency samples: 125900
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1368.05 txn/s, submitted: 1371.57 txn/s, failed submission: 3.53 txn/s, expired: 3.53 txn/s, latency: 2141.25 ms, (p50: 2100 ms, p70: 2400, p90: 2700 ms, p99: 3900 ms), latency samples: 124180
5. check swarm health
Compatibility test for 3c6e693a27339e73520f41030dce8fc9cd504967 ==> 19a9a1088d794667502fc76319f04648bd9f6ac5 passed
Upgrade the remaining nodes to version: 19a9a1088d794667502fc76319f04648bd9f6ac5
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1507.18 txn/s, submitted: 1509.65 txn/s, failed submission: 2.47 txn/s, expired: 2.47 txn/s, latency: 2030.29 ms, (p50: 2100 ms, p70: 2100, p90: 2400 ms, p99: 3600 ms), latency samples: 134200
Test Ok

@wrwg wrwg merged commit dd0dcd2 into main Dec 16, 2024
88 checks passed
@wrwg wrwg deleted the wrwg/type_info branch December 16, 2024 03:43
georgemitenkov pushed a commit that referenced this pull request Jan 6, 2025
@wrwg @georgemitenkov
[move-prover] Fix a bug in treatment of type reflection in spec funs (#…
83a5429 
…15606)

When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now.

Removes the boogie compilation error in #15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rahxephon89 rahxephon89 rahxephon89 approved these changes

@vineethk vineethk vineethk approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@wrwg @vineethk @rahxephon89